$\forall$$T$:Type, $f$:($T$$\rightarrow$$T$).
\\[0ex]retraction($T$;$f$) $\Rightarrow$ ($\forall$$L$:($T$ List), $x$, $y$:$T$. $x$=$f$$\ast$($y$) via $L$ $\Rightarrow$ no\_repeats($T$;$L$))